\section{Preliminaries}

\subsection{Basics}
\begin{frame}
\hframetitle{Basics}
\begin{lemma}[Update Semantics Basics]
For $\rho \in \Phi \cup \{\bot\}$
\begin{columns}
  \begin{column}{0.25\textwidth}
  \end{column}
  \begin{column}{0.75\textwidth}
    \begin{itemize}
    \item $\alpha[\rho] \sleq \alpha$
    \item  $\alpha \sleq \beta [\rho] \Longrightarrow \alpha =
      \alpha[\rho]$
    \item $\alpha \sleq \beta \Longrightarrow \alpha[\rho] \sleq \beta[\rho]$
    \item $\alpha = \beta \Longrightarrow \alpha[\rho] = \beta[\rho]$
    \item $\alpha [\rho][\rho] = \alpha [\rho]$
    \item $(\alpha \sqcap \beta)[\rho] = \alpha[\rho] \wedge
      \beta[\rho]$
    \end{itemize}
  \end{column}
\end{columns}
\end{lemma}
\end{frame}

\begin{frame}[allowframebreaks]
\proofframetitle{Basics (Proof)}

\begin{proof} \ \ \\
\begin{itemize}
  \item $\alpha[\rho] \sleq \alpha$
  \item $\alpha \sleq \beta [\rho] \Longrightarrow \alpha =
        \alpha[\rho]$
  \item $\alpha \sleq \beta \Longrightarrow \alpha[\rho] \sleq \beta[\rho]$
  \item $\alpha = \beta \Longrightarrow \alpha[\rho] = \beta[\rho]$
        \begin{center}\ldots these facts follow directly from the
        definitions for update semantics\ldots\end{center}
  \item $\alpha [\rho][\rho] = \alpha [\rho]$: Since $\alpha [\rho] \sleq
        \alpha[\rho]$, then by the above we have $\alpha [\rho] = \alpha[\rho]
        [\rho]$

\framebreak

  \item $(\alpha \sqcap \beta)[\rho] = \alpha[\rho] \sqcap
        \beta[\rho]$:  Observe that 
        \begin{align*}
          \alpha \sqcap \beta & \sleq \alpha \\ 
          \alpha \sqcap \beta & \sleq \beta 
        \end{align*}
        \ldots whence \ldots 
        \begin{align*}
          (\alpha \sqcap \beta)[\rho] & \sleq \alpha[\rho] \\ 
          (\alpha \sqcap \beta)[\rho] & \sleq \beta[\rho]
        \end{align*}
        \ldots therefore \ldots
        \begin{align}
          (\alpha \sqcap \beta)[\rho] & \sleq \alpha[\rho] \sqcap
          \beta[\rho] \label{basiceq1}
        \end{align}

\framebreak

        On the other hand, we have:
        \begin{align*} 
          \alpha[\rho] \sleq \alpha \\
          \beta[\rho] \sleq \beta
        \end{align*}
        \ldots thus \ldots 
        \begin{align*} 
          \alpha[\rho] \sqcap \beta[\rho] & \sleq \alpha \sqcap \beta
        \end{align*}

\framebreak

        \ldots moreover \ldots
        \begin{align} 
          (\alpha[\rho] \sqcap \beta[\rho])[\rho] & \sleq (\alpha \sqcap
          \beta)[\rho] \label{basiceq2}
        \end{align}
        However, we know that
        \[ \alpha[\rho] \sqcap \beta[\rho] \sleq \alpha[\rho] \]
        \ldots which means \ldots
        \begin{align} 
          \alpha[\rho] \sqcap \beta[\rho] & = (\alpha[\rho] \sqcap
          \beta[\rho])[\rho] \label{basiceq3}
        \end{align}
        And with \eqref{basiceq1}, \eqref{basiceq2}, and \eqref{basiceq3} we
        have enough to establish that indeed, $(\alpha\sqcap \beta)[\rho] =
        \alpha[\rho] \sqcap \beta[\rho]$
\end{itemize}
\end{proof}

\end{frame}

\subsection{$\Box$-Reduction}

\frame
{
  \hframetitle{$\Box$-Reduction}
As a warm up, we note the following, essentially trivial fact about
\alert{$\Box$}.  Despite its simplicity, however, it is a
\alert{reduction} of sorts.  We shall need to
appeal to this fact repeatedly in the completeness theorem\ldots
\mvspace{.5cm}
\begin{lemma}[$\Box$-Reduction]
\[ \alpha [\Box \phi] = \alpha \iff \alpha [\phi]= \alpha\]
\end{lemma}
}

\frame
{
  \proofframetitle{$\Box$-Reduction (Proof)}
\begin{proof}
This follows trivially by the definition of $\alpha [\Box \phi]$\ldots
\end{proof}
}

\subsection{General Reflection}
\frame{
\hframetitle{General Reflection}
Recall that the first property of the Veltman's abstract update
  semantics on Boolean lattices was \alert{reflection} --  this
property generalizes to all of the formulas we shall be concerned
with:
\mvspace{.5cm}
\begin{lemma}[General Reflection]
For all $\phi \in \mathcal{L}_0 \cup \mathcal{L}_\Box \cup
\mathcal{L}_\gillies$, we have:
\[ \alpha [\phi] \sleq \alpha \]
\end{lemma}
}

\begin{frame}[allowframebreaks]
\proofframetitle{General Reflection (Proof)}
%\renewcommand{\qedsymbol}{} 
\begin{proof}

The proof proceeds first by induction on complexity of $\phi$ in
$\mathcal{L}_0$, and then two further inductive cases for
$\mathcal{L}_\Box$ and $\mathcal{L}_\gillies$.
%\vfill

\mvspace{.5cm}

As a general strategy, it shall always suffice to show that $\alpha[\phi] = \alpha \wedge \alpha[\phi]$

%\vfill
\mvspace{.5cm}
  \begin{itemize}
\item $\rho \in \Phi \cup \{\bot\}$: This follows directly from fact that
  $\alpha[p] = \alpha\ll p\rr$ and $\ll p \rr$ is reflexive by
  postulate, and the fact that $\alpha[\bot] = \mathbf{0}$ and
  $\mathbf{0} \sleq \beta$ for all $\beta$
\framebreak
\item $\neg \phi$:

\mvspace{1cm} 
\begin{center}
   \includegraphics[]{tikz-proofs/proof2-crop.pdf}
\end{center} 

\framebreak

\item $\phi \wedge \psi$:

 \mvspace{1cm}
\begin{center}
   \includegraphics[]{tikz-proofs/proof1-crop.pdf}
\end{center}

\framebreak

\item $\Box \phi$ and $\phi \gillies \psi$:  We know that either
  $\alpha[\Box \phi] = \alpha$ or $\alpha[\Box \phi] = \mathbf{0}$,
  and likewise for $\gillies$.  Hence we know in either case that
  $\alpha[\Box \phi] \sleq \alpha$ and similarly $\alpha[\phi \gillies
  \psi ] \sleq \alpha$
\end{itemize}
\end{proof}
\end{frame}

\subsection{$\wedge$-Exportation}

\frame
{
  \hframetitle{$\wedge$-Exportation}
%\vfill
The following lemma establishes a key link between $\wedge$ and repeated update:
%\vfill
\mvspace{.5cm}
\begin{lemma}[$\wedge$-Exportation]
For all $\{\phi,\psi\} \subseteq \mathcal{L}_0$ we have:
\[ \alpha [\phi\wedge\psi] = \alpha [\phi][\psi] \]
\end{lemma}
%\vfill
}

\frame[allowframebreaks]
{
  \proofframetitle{$\wedge$-Exportation (Proof)}
%\renewcommand{\qedsymbol}{} 
\begin{proof}
The proof proceeds by \alert{induction on $\psi$}
\mvspace{.5cm} 
  \begin{itemize}
    \item $\rho \in \Phi \cup \{ \bot \}$:  First observe that $\alpha [\phi \wedge \rho] = \alpha [\phi] \wedge \alpha [\rho]$, and
since $\alpha [\phi] \wedge \alpha [\rho] \sqsubseteq \alpha [\rho]$ we have that $\alpha [\phi
\wedge \rho] \sqsubseteq \alpha [\rho]$.  But then it follows from the
basics of update semantics that:
%\mvspace{.5cm}
\begin{center}
  \includegraphics[]{tikz-proofs/proof3-crop.pdf}
\end{center}
%\end{itemize}
%\end{proof}
\framebreak
%\begin{proof}[]
%\begin{itemize}
 %   \item[]
On the other hand we have from the General Reflection Lemma that $\alpha
[\phi] = \alpha [\phi] \sqcap \alpha$, hence by the basics of update semantics
we have:
\mvspace{.5cm}
\begin{center}
  \includegraphics[]{tikz-proofs/proof4-crop.pdf}
\end{center}
%\end{itemize}
\mvspace{.5cm}
Taken together, we have then that $\alpha[\phi \wedge \rho] =
\alpha[\phi][\rho]$.
%\end{proof}
\framebreak
%\begin{proof}[]
%\begin{itemize}
  \item $\neg \psi$: Assume we have shown the result for $\psi$.  Observe the
following:
%\mvspace{.25cm}
%% Fucking graphic...
\mode<presentation>
{
  \begin{center}
    \includegraphics[width=0.8\textwidth]{tikz-proofs/proof5-crop.pdf}
  \end{center}
}
\mode<article>
{
  \begin{center}
    \includegraphics[]{tikz-proofs/proof5-crop.pdf}
  \end{center}
}
%\end{itemize}
%\end{proof}
\framebreak
%\renewcommand{\qedsymbol}{\textsquare}
%\begin{proof}[]
%\begin{itemize}
  \item $\psi \wedge \chi$:  Assume the result has been shown for $\psi$ and $\chi$.
Then we have the following:
%\mvspace{.25cm}
\begin{center}
  \includegraphics[]{tikz-proofs/proof6-crop.pdf}
\end{center}
\end{itemize}
This final inductive step completes the proof.
\end{proof}
}

\subsection{Gillies' Equivalence}

\frame
{
  \hframetitle{Gillies' Equivalence}

Let $\phi \to \psi$ abbreviate $ \neg (\phi \wedge \neg \psi)$.  In
\citep{gillies_epistemic_2004}, the following is offered as Prop. 4.2(b)
\mvspace{.5cm}
\begin{lemma}[Gillies' Equivalence]
For all $\{\phi,\psi\} \subseteq \mathcal{L}_0$ we have:
\[ \alpha [\phi \gillies \psi] = \alpha [\Box(\phi \to \psi)] \]
\end{lemma}
\mvspace{.5cm}
\ldots the above lemma serves to reduce the semantics of Gillies'
conditional to those of $\Box$, although it is of a different
character than the $\Box$-reduction lemma. 
}

\frame[allowframebreaks]
{
  \proofframetitle{Gillies' Equivalence (Proof)}
\begin{proof}
  First observe by $\Box$-reduction that we have the following:
\mvspace{.25cm}
\begin{center}
  \includegraphics[]{tikz-proofs/proof7-crop.pdf}
\end{center}
\framebreak
Thus we know that if $\alpha [\Box(\phi \rightarrow \psi)] = \alpha$ then
$\alpha [\phi \gillies \psi] = \alpha$, so then $\alpha [\Box(\phi \rightarrow \psi)]
= \alpha [\phi \gillies \psi]$.

\mvspace{.5cm}

On the other hand if $\alpha [\Box(\phi \rightarrow \psi)] \neq \alpha$ then
$\alpha [\Box(\phi \rightarrow \psi)] = \mathbf{0}$ and moreover $\alpha
[\phi \gillies \psi] \neq \alpha$, whence $\alpha [\phi \gillies \psi] = \mathbf{0}$,
hence $\alpha [\Box(\phi \rightarrow \psi)] = \alpha [\phi \gillies \psi]$. \ So no
matter what, we have the result.
\end{proof}
}

\subsection{$\gillies$-Reduction}

\frame
{
  \hframetitle{$\gillies$-Reduction}

%  Let $\phi \to \psi$ abbreviate $ \neg (\phi \wedge \neg \psi)$.
  \mvspace{.5cm}
  \begin{lemma}[$\gillies$-Reduction]
    For $\{\varphi, \psi\} \in \mathcal{L}_0$:
    \[\alpha[\varphi \gillies \psi] = \alpha \iff
      \alpha[\varphi \to \psi] = \alpha\]
  \end{lemma}
}

\frame
{
  \proofframetitle{$\gillies$-Reduction (Proof)}
  \begin{proof}
    This follows immediately from the Gillies' equivalence lemma and
    the $\Box$-reduction lemma.
  \end{proof}
}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "beamer"
%%% End: 
